g:IMonoid, i, j:.
(i < j)
 (E:({i..j}|g|). (*,e) i  k < j. E(k) = (E(i) * (*,e) i+1  k < j. E(k))  |g|) 

latex

Up	groups 1
Definitions of Statement	IMonoid
Definitions	t  T, x:A. B(x), False, A, P & Q, i  j < k, A  B, x. t(x), {T}, , x f y, x(s), {i..j}, P  Q, P  Q, P  Q, suptype(S; T), S  T, {i...}, IMonoid
Lemmas	imon wf, int upper wf, le wf, grp id wf, grp op wf, itop wf, grp car wf, int seg wf, int lt to int upper, int upper ind, itop unroll base, itop unroll unit, mon ident, itop unroll hi, mon assoc